Search Results

Documents authored by Salvati, Sylvain

Document
DOI: 10.4230/LIPIcs.ICDT.2024.17
Containment of Regular Path Queries Under Path Constraints

Authors: Sylvain Salvati and Sophie Tison

Published in: LIPIcs, Volume 290, 27th International Conference on Database Theory (ICDT 2024)

Abstract
Data integrity is ensured by expressing constraints it should satisfy. One can also view constraints as data properties and take advantage of them for several tasks such as reasoning about data or accelerating query processing. In the context of graph databases, simple constraints can be expressed by means of path constraints while simple queries are modeled as regular path queries (RPQs). In this paper, we investigate the containment of RPQs under path constraints. We focus on word constraints that can be viewed as tuple-generating dependencies (TGDs) of the form ∀x_1,x_2, ∃y⁻, a_1(x_1,y_1) ∧ ... ∧ a_i(y_{i-1},y_i) ∧ ... ∧ a_n(y_{n-1},x_2) ⟶ ∃z⁻, b_1(x_1,z_1) ∧ ... ∧ b_i(z_{i-1},z_i) ∧ ... ∧ b_m(z_{m-1},x_2). Such a constraint means that whenever two nodes in a graph are connected by a path labeled a_1 … a_n, there is also a path labeled b_1 … b_m that connects them. Rewrite systems offer an abstract view of these TGDs: the rewrite rule a_1 … a_n → b_1 … b_m represents the previous constraint. A set of constraints 𝒞 is then represented by a rewrite system R and, when dealing with possibly infinite databases, a path query p is contained in a path query q under the constraints 𝒞 iff p rewrites to q with R. Contrary to what has been claimed in the literature we show that, when restricting to finite databases only, there are cases where a path query p is contained in a path query q under the constraints 𝒞 while p does not rewrite to q with R. More generally, we study the finite controllability of the containment of RPQs under word constraints, that is when this containment problem on unrestricted databases does coincide with the finite case. We give an exact characterisation of the cases where this equivalence holds. We then deduce the undecidability of the containment problem in the finite case even when RPQs are restricted to word queries. We prove several properties related to finite controllability, and in particular that it is undecidable. We also exhibit some classes of word constraints that ensure the finite controllability and the decidability of the containment problem.
Cite as

Sylvain Salvati and Sophie Tison. Containment of Regular Path Queries Under Path Constraints. In 27th International Conference on Database Theory (ICDT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 290, pp. 17:1-17:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{salvati_et_al:LIPIcs.ICDT.2024.17,
  author =	{Salvati, Sylvain and Tison, Sophie},
  title =	{{Containment of Regular Path Queries Under Path Constraints}},
  booktitle =	{27th International Conference on Database Theory (ICDT 2024)},
  pages =	{17:1--17:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-312-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{290},
  editor =	{Cormode, Graham and Shekelyan, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2024.17},
  URN =		{urn:nbn:de:0030-drops-197994},
  doi =		{10.4230/LIPIcs.ICDT.2024.17},
  annote =	{Keywords: Graph databases, rational path queries, query containment, TGDs, word constraints, rewrite systems, finite controllability, decision problems}
}
Document
DOI: 10.4230/LIPIcs.STACS.2023.51
An Algebraic Approach to Vectorial Programs

Authors: Charles Paperman, Sylvain Salvati, and Claire Soyez-Martin

Published in: LIPIcs, Volume 254, 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)

Abstract
Vectorial programming, the combination of SIMD instructions with usual processor instructions, is known to speed-up many standard algorithms. Simple regular languages have benefited from this technology. This paper is a first step towards pushing these benefits further. We take advantage of the inner algebraic structure of regular languages and produce high level representations of efficient vectorial programs that recognize certain classes of regular languages. As a technical ingredient, we establish equivalences between classes of vectorial circuits and logical formalisms, namely unary temporal logic and first order logic. The main result is the construction of compilation procedures that turns syntactic semigroups into vectorial circuits. The circuits we obtain are small in that they improve known upper-bounds on representations of automata within the logical formalisms. The gain is mostly due to a careful sharing of sub-formulas based on algebraic tools.
Cite as

Charles Paperman, Sylvain Salvati, and Claire Soyez-Martin. An Algebraic Approach to Vectorial Programs. In 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 254, pp. 51:1-51:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{paperman_et_al:LIPIcs.STACS.2023.51,
  author =	{Paperman, Charles and Salvati, Sylvain and Soyez-Martin, Claire},
  title =	{{An Algebraic Approach to Vectorial Programs}},
  booktitle =	{40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)},
  pages =	{51:1--51:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-266-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{254},
  editor =	{Berenbrink, Petra and Bouyer, Patricia and Dawar, Anuj and Kant\'{e}, Mamadou Moustapha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2023.51},
  URN =		{urn:nbn:de:0030-drops-177030},
  doi =		{10.4230/LIPIcs.STACS.2023.51},
  annote =	{Keywords: Automata theory, Semigroups, Vectorisation}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2020.38
Linear High-Order Deterministic Tree Transducers with Regular Look-Ahead

Authors: Paul D. Gallot, Aurélien Lemay, and Sylvain Salvati

Published in: LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

Abstract
We introduce the notion of high-order deterministic top-down tree transducers (HODT) whose outputs correspond to single-typed lambda-calculus formulas. These transducers are natural generalizations of known models of top-tree transducers such as: Deterministic Top-Down Tree Transducers, Macro Tree Transducers, Streaming Tree Transducers... We focus on the linear restriction of high order tree transducers with look-ahead (HODTR_lin), and prove this corresponds to tree to tree functional transformations defined by Monadic Second Order (MSO) logic. We give a specialized procedure for the composition of those transducers that uses a flow analysis based on coherence spaces and allows us to preserve the linearity of transducers. This procedure has a better complexity than classical algorithms for composition of other equivalent tree transducers, but raises the order of transducers. However, we also indicate that the order of a HODTR_lin can always be bounded by 3, and give a procedure that reduces the order of a HODTR_lin to 3. As those resulting HODTR_lin can then be transformed into other equivalent models, this gives an important insight on composition algorithm for other classes of transducers. Finally, we prove that those results partially translate to the case of almost linear HODTR: the class corresponds to the class of tree transformations performed by MSO with unfolding (not closed by composition), and provide a mechanism to reduce the order to 3 in this case.
Cite as

Paul D. Gallot, Aurélien Lemay, and Sylvain Salvati. Linear High-Order Deterministic Tree Transducers with Regular Look-Ahead. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 38:1-38:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{gallot_et_al:LIPIcs.MFCS.2020.38,
  author =	{Gallot, Paul D. and Lemay, Aur\'{e}lien and Salvati, Sylvain},
  title =	{{Linear High-Order Deterministic Tree Transducers with Regular Look-Ahead}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{38:1--38:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Esparza, Javier and Kr\'{a}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.38},
  URN =		{urn:nbn:de:0030-drops-127050},
  doi =		{10.4230/LIPIcs.MFCS.2020.38},
  annote =	{Keywords: Transducers, \lambda-calculus, Trees}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2018.44
On the Boundedness Problem for Higher-Order Pushdown Vector Addition Systems

Authors: Vincent Penelle, Sylvain Salvati, and Grégoire Sutre

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract
Karp and Miller's algorithm is a well-known decision procedure that solves the termination and boundedness problems for vector addition systems with states (VASS), or equivalently Petri nets. This procedure was later extended to a general class of models, well-structured transition systems, and, more recently, to pushdown VASS. In this paper, we extend pushdown VASS to higher-order pushdown VASS (called HOPVASS), and we investigate whether an approach à la Karp and Miller can still be used to solve termination and boundedness. We provide a decidable characterisation of runs that can be iterated arbitrarily many times, which is the main ingredient of Karp and Miller's approach. However, the resulting Karp and Miller procedure only gives a semi-algorithm for HOPVASS. In fact, we show that coverability, termination and boundedness are all undecidable for HOPVASS, even in the restricted subcase of one counter and an order 2 stack. On the bright side, we prove that this semi-algorithm is in fact an algorithm for higher-order pushdown automata.
Cite as

Vincent Penelle, Sylvain Salvati, and Grégoire Sutre. On the Boundedness Problem for Higher-Order Pushdown Vector Addition Systems. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 44:1-44:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{penelle_et_al:LIPIcs.FSTTCS.2018.44,
  author =	{Penelle, Vincent and Salvati, Sylvain and Sutre, Gr\'{e}goire},
  title =	{{On the Boundedness Problem for Higher-Order Pushdown Vector Addition Systems}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{44:1--44:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.44},
  URN =		{urn:nbn:de:0030-drops-99432},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.44},
  annote =	{Keywords: Higher-order pushdown automata, Vector addition systems, Boundedness problem, Termination problem, Coverability problem}
}
Document
DOI: 10.4230/LIPIcs.STACS.2017.34
On the Decomposition of Finite-Valued Streaming String Transducers

Authors: Paul Gallot, Anca Muscholl, Gabriele Puppis, and Sylvain Salvati

Published in: LIPIcs, Volume 66, 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)

Abstract
We prove the following decomposition theorem: every 1-register streaming string transducer that associates a uniformly bounded number of outputs with each input can be effectively decomposed as a finite union of functional 1-register streaming string transducers. This theorem relies on a combinatorial result by Kortelainen concerning word equations with iterated factors. Our result implies the decidability of the equivalence problem for the considered class of transducers. This can be seen as a first step towards proving a more general decomposition theorem for streaming string transducers with multiple registers.
Cite as

Paul Gallot, Anca Muscholl, Gabriele Puppis, and Sylvain Salvati. On the Decomposition of Finite-Valued Streaming String Transducers. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 34:1-34:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{gallot_et_al:LIPIcs.STACS.2017.34,
  author =	{Gallot, Paul and Muscholl, Anca and Puppis, Gabriele and Salvati, Sylvain},
  title =	{{On the Decomposition of Finite-Valued Streaming String Transducers}},
  booktitle =	{34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)},
  pages =	{34:1--34:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-028-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{66},
  editor =	{Vollmer, Heribert and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2017.34},
  URN =		{urn:nbn:de:0030-drops-69997},
  doi =		{10.4230/LIPIcs.STACS.2017.34},
  annote =	{Keywords: Streaming Transducers, finite valuedness, equivalence}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.163
Ordered Tree-Pushdown Systems

Authors: Lorenzo Clemente, Pawel Parys, Sylvain Salvati, and Igor Walukiewicz

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
We define a new class of pushdown systems where the pushdown is a tree instead of a word. We allow a limited form of lookahead on the pushdown conforming to a certain ordering restriction, and we show that the resulting class enjoys a decidable reachability problem. This follows from a preservation of recognizability result for the backward reachability relation of such systems. As an application, we show that our simple model can encode several formalisms generalizing pushdown systems, such as ordered multi-pushdown systems, annotated higher-order pushdown systems, the Krivine machine, and ordered annotated multi-pushdown systems. In each case, our procedure yields tight complexity.
Cite as

Lorenzo Clemente, Pawel Parys, Sylvain Salvati, and Igor Walukiewicz. Ordered Tree-Pushdown Systems. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 163-177, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{clemente_et_al:LIPIcs.FSTTCS.2015.163,
  author =	{Clemente, Lorenzo and Parys, Pawel and Salvati, Sylvain and Walukiewicz, Igor},
  title =	{{Ordered Tree-Pushdown Systems}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{163--177},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.163},
  URN =		{urn:nbn:de:0030-drops-56470},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.163},
  annote =	{Keywords: reachability analysis, saturation technique, pushdown automata, ordered pushdown automata, higher-order pushdown automata, higher-order recursive sche}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.229
A Model for Behavioural Properties of Higher-order Programs

Authors: Sylvain Salvati and Igor Walukiewicz

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
We consider simply typed lambda-calculus with fixpoints as a non-interpreted functional programming language: the result of the execution of a program is its normal form that can be seen as a potentially infinite tree of calls to built-in operations. Properties of such trees are properties of executions of programs and monadic second-order logic (MSOL) is well suited to express them. For a given MSOL property we show how to construct a finitary model recognizing it. In other words, the value of a lambda-term in the model determines if the tree that is the result of the execution of the term satisfies the property. The finiteness of the construction has as consequences many known results about the verification of higher-order programs in this framework.
Cite as

Sylvain Salvati and Igor Walukiewicz. A Model for Behavioural Properties of Higher-order Programs. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 229-243, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{salvati_et_al:LIPIcs.CSL.2015.229,
  author =	{Salvati, Sylvain and Walukiewicz, Igor},
  title =	{{A Model for Behavioural Properties of Higher-order Programs}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{229--243},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.229},
  URN =		{urn:nbn:de:0030-drops-54173},
  doi =		{10.4230/LIPIcs.CSL.2015.229},
  annote =	{Keywords: Simply typed lambda-Y-calculus, Monadic second order logic, semantic models}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2013.103
Evaluation is MSOL-compatible

Authors: Sylvain Salvati and Igor Walukiewicz

Published in: LIPIcs, Volume 24, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)

Abstract
We consider simply-typed lambda calculus with fixpoint operators. Evaluation of a term gives as a result the Böhm tree of the term. We show that evaluation is compatible with monadic second-order logic (MSOL). This means that for a fixed finite vocabulary of terms, the MSOL properties of Böhm trees of terms are effectively MSOL properties of terms themselves. Theorems of this kind have been known for some graph operations: unfolding, and Muchnik iteration. Similarly to those results, our main theorem has diverse applications. It can be used to show decidability results, to construct classes of graphs with decidable MSOL theory, or to obtain MSOL formulas expressing behavioral properties of terms. Another application is decidability of a control-flow synthesis problem.
Cite as

Sylvain Salvati and Igor Walukiewicz. Evaluation is MSOL-compatible. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 103-114, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{salvati_et_al:LIPIcs.FSTTCS.2013.103,
  author =	{Salvati, Sylvain and Walukiewicz, Igor},
  title =	{{Evaluation is MSOL-compatible}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)},
  pages =	{103--114},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-64-4},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{24},
  editor =	{Seth, Anil and Vishnoi, Nisheeth K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.103},
  URN =		{urn:nbn:de:0030-drops-43652},
  doi =		{10.4230/LIPIcs.FSTTCS.2013.103},
  annote =	{Keywords: Simply typed \$lambda Y\$-calculus; Monadic second order}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact